A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$
Identifieur interne : 001661 ( Main/Exploration ); précédent : 001660; suivant : 001662A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$
Auteurs : Mohammad Khodadadi [Royaume-Uni] ; Renate A. Schmidt [Royaume-Uni] ; Dmitry Tishkovsky [Royaume-Uni]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The paper presents a tableau calculus with several refinements for reasoning in the description logic $\mathcal{SHOI}$ . The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, we use a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTel. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance.
Url:
DOI: 10.1007/978-3-642-40537-2_17
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003B55
- to stream Istex, to step Curation: 003B11
- to stream Istex, to step Checkpoint: 000287
- to stream Main, to step Merge: 001673
- to stream Main, to step Curation: 001661
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$</title><author><name sortKey="Khodadadi, Mohammad" sort="Khodadadi, Mohammad" uniqKey="Khodadadi M" first="Mohammad" last="Khodadadi">Mohammad Khodadadi</name></author><author><name sortKey="Schmidt, Renate A" sort="Schmidt, Renate A" uniqKey="Schmidt R" first="Renate A." last="Schmidt">Renate A. Schmidt</name></author><author><name sortKey="Tishkovsky, Dmitry" sort="Tishkovsky, Dmitry" uniqKey="Tishkovsky D" first="Dmitry" last="Tishkovsky">Dmitry Tishkovsky</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:F889B235A22359EC3C33AC9007DF2915FC3A6BA3</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-40537-2_17</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-5L1FMW81-D/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003B55</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003B55</idno><idno type="wicri:Area/Istex/Curation">003B11</idno><idno type="wicri:Area/Istex/Checkpoint">000287</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000287</idno><idno type="wicri:doubleKey">0302-9743:2013:Khodadadi M:a:refined:tableau</idno><idno type="wicri:Area/Main/Merge">001673</idno><idno type="wicri:Area/Main/Curation">001661</idno><idno type="wicri:Area/Main/Exploration">001661</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Refined Tableau Calculus with Controlled Blocking for the Description Logic <formula xml:id="IEq1" notation="TEX"><media mimeType="image" url=""></media>
$\mathcal{SHOI}$
</formula></title><author><name sortKey="Khodadadi, Mohammad" sort="Khodadadi, Mohammad" uniqKey="Khodadadi M" first="Mohammad" last="Khodadadi">Mohammad Khodadadi</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, The University of Manchester</wicri:regionArea><placeName><settlement type="city">Manchester</settlement><region type="nation">Angleterre</region><region nuts="2" type="region">Grand Manchester</region></placeName><orgName type="university">Université de Manchester</orgName></affiliation></author><author><name sortKey="Schmidt, Renate A" sort="Schmidt, Renate A" uniqKey="Schmidt R" first="Renate A." last="Schmidt">Renate A. Schmidt</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, The University of Manchester</wicri:regionArea><placeName><settlement type="city">Manchester</settlement><region type="nation">Angleterre</region><region nuts="2" type="region">Grand Manchester</region></placeName><orgName type="university">Université de Manchester</orgName></affiliation></author><author><name sortKey="Tishkovsky, Dmitry" sort="Tishkovsky, Dmitry" uniqKey="Tishkovsky D" first="Dmitry" last="Tishkovsky">Dmitry Tishkovsky</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, The University of Manchester</wicri:regionArea><placeName><settlement type="city">Manchester</settlement><region type="nation">Angleterre</region><region nuts="2" type="region">Grand Manchester</region></placeName><orgName type="university">Université de Manchester</orgName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The paper presents a tableau calculus with several refinements for reasoning in the description logic $\mathcal{SHOI}$ . The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, we use a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTel. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance.</div></front></TEI><affiliations><list><country><li>Royaume-Uni</li></country><region><li>Angleterre</li><li>Grand Manchester</li></region><settlement><li>Manchester</li></settlement><orgName><li>Université de Manchester</li></orgName></list><tree><country name="Royaume-Uni"><region name="Angleterre"><name sortKey="Khodadadi, Mohammad" sort="Khodadadi, Mohammad" uniqKey="Khodadadi M" first="Mohammad" last="Khodadadi">Mohammad Khodadadi</name></region><name sortKey="Schmidt, Renate A" sort="Schmidt, Renate A" uniqKey="Schmidt R" first="Renate A." last="Schmidt">Renate A. Schmidt</name><name sortKey="Tishkovsky, Dmitry" sort="Tishkovsky, Dmitry" uniqKey="Tishkovsky D" first="Dmitry" last="Tishkovsky">Dmitry Tishkovsky</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001661 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001661 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:F889B235A22359EC3C33AC9007DF2915FC3A6BA3
|texte= A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$
}}
| This area was generated with Dilib version V0.6.33. |  |